mcsta/modest mcsta zeroconf.jani -E N=1000,K=8,reset=false --props correct_max -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --p0 --p1 --epsilon 0 --absolute-epsilon
zeroconf.jani:model: info: zeroconf is an MDP model.
zeroconf.jani:variables[21]: info: Expanding variable "l" into 5 locations in automaton "host0".
zeroconf.jani: info: Need 24 bytes per state.
zeroconf.jani: info: Explored 1868787 states for N=1000, K=8, reset=False.
Peak memory usage: 665 MB
Analysis results for zeroconf.jani
Experiment N=1000, K=8, reset=False
+ State space exploration
State size: 24 bytes
States: 1868787
Transitions: 3430379
Branches: 4224736
Rate: 394675 states/s
Time: 5.0 s
+ Property correct_max
Probability: 4.801413635072433E-08
Bounds: [4.801413635072433E-08, 4.801413635072433E-08]
Time: 207.3 s
+ Precomputations
Max. prob. 0 states: 611330
Time for max. prob. 0 states: 0.8 s
Max. prob. 1 states: 170198
Time for max. prob. 1 states: 200.9 s
+ Essential states
Iterations: 37
Essential states: 752938
Transitions: 1621174
Branches: 2104946
Time: 3.7 s
+ Value iteration
Final error: 0
Iterations: 33
Time: 1.9 s
Exported results to file "/out.txt".